Issue3592-1.agda:5,1-10,20
P is not strictly positive, because it occurs
in the first argument of f
in the first argument of P
(in the first clause
 in the definition of Q), which is
an index of P.
